es:event_system{i:l}, i,x:Id, T:Type. es-dtype(es; i; x; T)  prop{i:l} 

latex

Definitions	event_system{i:l}, t  T, Id, Type, x:A. B(x), es-vartype(es; i; x), es-isconst(es; i; x), b, prop{i:l}, x:A  B(x), P  Q, es-dtype(es; i; x; T)
Lemmas	assert wf, es-isconst wf, subtype rel wf, es-vartype wf, Id wf, event system wf